app2(id, x) -> x
app2(plus, 0) -> id
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
↳ QTRS
↳ DependencyPairsProof
app2(id, x) -> x
app2(plus, 0) -> id
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
APP2(app2(plus, app2(s, x)), y) -> APP2(s, app2(app2(plus, x), y))
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
APP2(app2(plus, app2(s, x)), y) -> APP2(plus, x)
app2(id, x) -> x
app2(plus, 0) -> id
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APP2(app2(plus, app2(s, x)), y) -> APP2(s, app2(app2(plus, x), y))
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
APP2(app2(plus, app2(s, x)), y) -> APP2(plus, x)
app2(id, x) -> x
app2(plus, 0) -> id
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
app2(id, x) -> x
app2(plus, 0) -> id
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP2(app2(plus, app2(s, x)), y) -> APP2(app2(plus, x), y)
POL(0) = 0
POL(APP2(x1, x2)) = 2·x1
POL(app2(x1, x2)) = x1 + 2·x2
POL(id) = 0
POL(plus) = 1
POL(s) = 1
app2(plus, 0) -> id
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
app2(id, x) -> x
app2(plus, 0) -> id
app2(app2(plus, app2(s, x)), y) -> app2(s, app2(app2(plus, x), y))